package kodkod.analysis;

import java.util.*;

import kodkod.ast.*;
import kodkod.ast.operator.ExprOperator;
import kodkod.instance.TupleSet;

public class PositiveLeafs extends HashSet<LeafExpression> {
	
	boolean includeDeclarations = false;
	
	public PositiveLeafs() { super(); }
	
	public PositiveLeafs(ComparisonFormula f) {
		this(f, false);
	}
	
	public PositiveLeafs(Decl f) {
		this(f, false);
	}
	
	public PositiveLeafs(Expression exp) {
		this(exp, false);
	}
	
	public PositiveLeafs(IntExpression exp) {
		this(exp, false); 
	}
	
	public PositiveLeafs(IntComparisonFormula f) {
		this(f, false);
	}
	
	public PositiveLeafs(IntComparisonFormula f, boolean includeDeclarations) {
		super();
		this.includeDeclarations = includeDeclarations;
		
		this.addAll(new PositiveLeafs(f.left(), includeDeclarations));
		this.addAll(new PositiveLeafs(f.right(), includeDeclarations));
	}
	
	public PositiveLeafs(ComparisonFormula f, boolean includeDeclarations) {
		super();
		this.includeDeclarations = includeDeclarations;
		
		this.addAll(new PositiveLeafs(f.left(), includeDeclarations));
		this.addAll(new PositiveLeafs(f.right(), includeDeclarations));
	}
	
	public PositiveLeafs(Decl f, boolean includeDeclarations) {
		super();
		this.includeDeclarations = includeDeclarations;
		
		this.addAll(new PositiveLeafs(f.expression(), includeDeclarations));
		this.addAll(new PositiveLeafs(f.variable(), includeDeclarations));
	}
	
	public PositiveLeafs(Expression exp, boolean includeDeclarations) {
		super();
		this.includeDeclarations = includeDeclarations;
		
		if (exp instanceof UnaryExpression) {
			UnaryExpression e = (UnaryExpression)exp;
			this.addAll(new PositiveLeafs(e.expression(), includeDeclarations));
		}
		else if (exp instanceof BinaryExpression) {
			BinaryExpression e = (BinaryExpression)exp;
			this.addAll(new PositiveLeafs(e.left(), includeDeclarations));
			if (!e.op().equals(ExprOperator.DIFFERENCE)) {
				this.addAll(new PositiveLeafs(e.right(), includeDeclarations));
			}
		}
		else if (exp instanceof NaryExpression) {
			NaryExpression e = (NaryExpression)exp;
			for (Expression child : e) {
				this.addAll(new PositiveLeafs(child, includeDeclarations));
			}
		}
		else if (exp instanceof Comprehension) {
			Comprehension e = (Comprehension)exp;
			if (includeDeclarations) {
				for (Decl child : e.decls()) {
					this.addAll(new PositiveLeafs(child.expression(), includeDeclarations));
				}
			}
		}
		else if (exp instanceof IfExpression) {
			IfExpression e = (IfExpression)exp;
			this.addAll(new PositiveLeafs(e.thenExpr(), includeDeclarations));
			this.addAll(new PositiveLeafs(e.elseExpr(), includeDeclarations));
		}
		else if (exp instanceof ProjectExpression) {
			ProjectExpression e = (ProjectExpression)exp;
			this.addAll(new PositiveLeafs(e.expression(), includeDeclarations));
		}
		else if (exp instanceof IntToExprCast) {
			IntToExprCast e = (IntToExprCast)exp;
		}
		else if (exp instanceof LeafExpression) {
			if (exp instanceof ConstantExpression) {
				ConstantExpression e = (ConstantExpression)exp;
			} 
			else if (exp instanceof Relation) {
				Relation e = (Relation)exp;
				if (Analyzer.translation.primaryRelations.contains(e)) {
					this.add(e);
				}
			}
			else if (exp instanceof Variable) {
				Variable var = (Variable)exp;
				if (Analyzer.translation.skolemRelations.containsKey(var)) { 
					this.add(var);
				}
				else if (includeDeclarations) {
					Expression e = Analyzer.initialAnalysis.decls.get(var);
					this.addAll(new PositiveLeafs(e, includeDeclarations));
				}
			}
		}
	}
	
	public PositiveLeafs(IntExpression exp, boolean includeDeclarations) {
		super();
		this.includeDeclarations = includeDeclarations;
		
		if (exp instanceof UnaryIntExpression) {
			UnaryIntExpression e = (UnaryIntExpression)exp;
			this.addAll(new PositiveLeafs(e.intExpr(), includeDeclarations));
		} else if (exp instanceof BinaryIntExpression) {
			BinaryIntExpression e = (BinaryIntExpression)exp;
			this.addAll(new PositiveLeafs(e.left(), includeDeclarations));
			this.addAll(new PositiveLeafs(e.right(), includeDeclarations));
		} else if (exp instanceof NaryIntExpression) {
			NaryIntExpression e = (NaryIntExpression)exp;
			for (IntExpression child : e) this.addAll(new PositiveLeafs(child, includeDeclarations));
		} else if (exp instanceof SumExpression) {
			SumExpression e = (SumExpression)exp;
			this.addAll(new PositiveLeafs(((SumExpression) exp).intExpr()));
			for (Decl decl : e.decls()) this.addAll(new PositiveLeafs(decl, includeDeclarations));
		} else if (exp instanceof IfIntExpression) {
			IfIntExpression e = (IfIntExpression)exp;
			this.addAll(new PositiveLeafs(e.thenExpr(), includeDeclarations));
			this.addAll(new PositiveLeafs(e.elseExpr(), includeDeclarations));
		} else if (exp instanceof ExprToIntCast) {
			ExprToIntCast e = (ExprToIntCast)exp;
			this.addAll(new PositiveLeafs(e.expression(), includeDeclarations));
		} else if (exp instanceof IntConstant) {
			IntConstant e = (IntConstant)exp;
		} 
	}
	
	public int childsize() {
		int childsize = 0;
		for (LeafExpression leaf : this) {
			if (childsize(leaf) < 0) {
				throw new RuntimeException(leaf.name());
			}
			childsize += childsize(leaf);
		}
		return childsize;
	}
	
	public static int childsize(LeafExpression leaf) {
		Relation r = null;
		
		if (leaf instanceof Relation) {
			r = (Relation)leaf;
		}
		else if (leaf instanceof Variable) {
			Variable var = (Variable)leaf;
			r = Analyzer.translation.skolemRelations.get(var);
		}
		
		TupleSet upper = Analyzer.translation.bounds.upperBound(r);
		TupleSet lower = Analyzer.translation.bounds.lowerBound(r);
		return upper.size() - lower.size();
	}
}
